1  (CONTEXT (1 0) 1 0)
2  (ASSERT (EQ AA (TIMES QQ YY)) WRT $VERICON)
3  TRUE
4  (ASSERT (EQ (TIMES 2 BB) (TIMES QQ DD)) WRT $VERICON)
5  TRUE
6  (ASSERT (LT PP (PLUS (TIMES QQ YY) (TIMES QQ DD))) WRT $VERICON)
7  (ASSERT (LTQ (PLUS 1 $X) $Y) WRT $VERICON)
8  TRUE
9  (ASSERT (LTQ (TIMES QQ YY) PP) WRT $VERICON)
10 TRUE
11 (ASSERT (LT PP (PLUS AA BB)) WRT $VERICON)
12 (ASSERT (LTQ (PLUS 1 $X) $Y) WRT $VERICON)
13 TRUE
14 (DENY (LT (DIVIDES DD 2) EE) WRT $VERICON)
15 FLASE
16 (GOAL $PROVE (LT PP (PLUS (TIMES QQ YY) (TIMES QQ (DIVIDES DD 2))))
WRT $VERICON)
17   LAMBDA PROOFSWITCH (LT PP (PLUS (TIMES QQ YY) (TIMES QQ (DIVIDES
DD 2))))
18   (GOAL $INEQUALITIES ($F $X))
19     LAMBDA RELCHECK (LT PP (PLUS (TIMES QQ YY) (TIMES QQ (DIVIDES
DD 2))))
20     LAMBDA PROOFSIMP (LT PP (PLUS (TIMES QQ YY) (TIMES QQ (DIVIDES
DD 2))))
21       LAMBDA ARGSIMP (LT PP (PLUS (TIMES QQ YY) (TIMES QQ (DIVIDES
DD 2))))
22         LAMBDA SIMPONE (TUPLE PP (PLUS (TIMES QQ YY) (TIMES QQ
(DIVIDES DD 2))))
(TUPLE PP (PLUS (TIMES QQ YY) (TIMES QQ (DIVIDES DD 2))))
SIMPLIFY?
:N
23         (FAIL)
24     (FAIL)
25     LAMBDA PROOFLEIB (LT PP (PLUS (TIMES QQ YY) (TIMES QQ (DIVIDES
DD 2))))
26     (EXISTS ($F ←Y))
(EQ (TUPLE PP (PLUS (TIMES QQ YY) (TIMES QQ (DIVIDES DD 2)))) (TUPLE
PP (PLUS (TIMES QQ YY) (TIMES QQ DD))))
PROVE?
:N
27     (FAIL)
(EQ (TUPLE PP (PLUS (TIMES QQ YY) (TIMES QQ (DIVIDES DD 2)))) (TUPLE
PP (PLUS AA BB)))
PROVE?
:N
28     (FAIL)
29     LAMBDA INEQLEIB (LT PP (PLUS (TIMES QQ YY) (TIMES QQ (DIVIDES
DD 2))))
30     (EXISTS ($L (TUPLE ←LOWER ←UPPER)))
PROVE
(LTQ PP PP)
AND
(LTQ (PLUS (TIMES QQ YY) (TIMES QQ DD)) (PLUS (TIMES QQ YY) (TIMES
QQ (DIVIDES DD 2))))
?
:N
31     (FAIL)
PROVE
(LTQ PP PP)
AND
(LTQ (PLUS AA BB) (PLUS (TIMES QQ YY) (TIMES QQ (DIVIDES DD 2))))
?
:Y
32     (GOAL $INEQUALITIES (AND (LTQ $X $LOWER) (LTQ $UPPER $Y)))
33       LAMBDA ANDSPLIT (AND (LTQ PP PP) (LTQ (PLUS AA BB) (PLUS
(TIMES QQ YY) (TIMES QQ (DIVIDES DD 2)))))
34       (GOAL $GOALCLASS $X)
35         LAMBDA RELCHECK (LTQ PP PP)
36         RELCHECK = TRUE
37       (GOAL $GOALCLASS (AND $$Y))
38         LAMBDA ANDSPLIT (AND (LTQ (PLUS AA BB) (PLUS (TIMES QQ
YY) (TIMES QQ (DIVIDES DD 2)))))
39         (GOAL $GOALCLASS $X)
40           LAMBDA RELCHECK (LTQ (PLUS AA BB) (PLUS (TIMES QQ YY)
(TIMES QQ (DIVIDES DD 2))))
41           LAMBDA EQINEQMONOTONE (LTQ (PLUS AA BB) (PLUS (TIMES
QQ YY) (TIMES QQ (DIVIDES DD 2))))
42             LAMBDA INSIST TRUE
43             INSIST = TRUE
PROVE
(LTQ AA (TIMES QQ (DIVIDES DD 2)))
AND
(LTQ BB (TIMES QQ YY))
?
:N
44           (FAIL)
45           LAMBDA EQINEQMONOTONE (LTQ (PLUS AA BB) (PLUS (TIMES
QQ YY) (TIMES QQ (DIVIDES DD 2))))
46             LAMBDA INSIST TRUE
47             INSIST = TRUE
PROVE
(LTQ AA (TIMES QQ YY))
AND
(LTQ BB (TIMES QQ (DIVIDES DD 2)))
?
:Y
48           (GOAL $GOALCLASS (AND ($L (TUPLE $W $Y)) ($L (TUPLE $X
$Z))))
49             LAMBDA ANDSPLIT (AND (LTQ AA (TIMES QQ YY)) (LTQ BB
(TIMES QQ (DIVIDES DD 2))))
50             (GOAL $GOALCLASS $X)
51               LAMBDA RELCHECK (LTQ AA (TIMES QQ YY))
52               RELCHECK = TRUE
53             (GOAL $GOALCLASS (AND $$Y))
54               LAMBDA ANDSPLIT (AND (LTQ BB (TIMES QQ (DIVIDES DD
2))))
55               (GOAL $GOALCLASS $X)
56                 LAMBDA RELCHECK (LTQ BB (TIMES QQ (DIVIDES DD 2)))
57                 LAMBDA INEQTIMESDIVIDE (LTQ BB (TIMES QQ (DIVIDES
DD 2)))
58                 (GOAL $DEDUCE (LT 0 $Y))
59                   LAMBDA RELCHECK (LT 0 2)
60                   RELCHECK = TRUE
61                 (GOAL $INEQUALITIES ($F (TUPLE (TIMES $Y $W) (TIMES
$X $$Z))))
62                   LAMBDA RELCHECK (LTQ (TIMES 2 BB) (TIMES QQ DD))
63                   RELCHECK = TRUE
64                 INEQTIMESDIVIDE = TRUE
65               (GOAL $GOALCLASS (AND $$Y))
66               ANDSPLIT = (AND)
67             ANDSPLIT = (AND)
68           EQINEQMONOTONE = (AND)
69         (GOAL $GOALCLASS (AND $$Y))
70         ANDSPLIT = (AND)
71       ANDSPLIT = (AND)
72     INEQLEIB = (AND)
73   (ASSERT ($F $X))
74   (ASSERT (LTQ (PLUS 1 $X) $Y) WRT $VERICON)
75   PROOFSWITCH = (LT PP (PLUS (TIMES QQ YY) (TIMES QQ (DIVIDES DD
2))))
76 (LT PP (PLUS (TIMES QQ YY) (TIMES QQ (DIVIDES DD 2))))